ltg:(IdLnkIdType), i:Id, da1, da2:k:Knd fp Type.
(ltg  da-outlinks(da1  da2;i))  (ltg  da-outlinks(da1;i))  (ltg  da-outlinks(da2;i)) 

latex

Definitions

{T}, Unit, , b, lnk(k), tag(k), f(x), , AB, A, False, ||as||, l[i], Prop, mapfilter(f;P;L), SqStable(P), T, True, Dec(P), x:A. B(x), lexpr{i}, Knd, b, x  dom(f), has-src(i;k), IdLnk, Id, da-outlink-f(da;k), fpf-dom-list(f), f  g, KindDeq, P  Q, (x  l), da-outlinks(da;i), a:A fp B(a), A & B, isrcv(k), P  Q, P & Q, P  Q, P  Q, x. t(x), x:A. B(x), t  T, Top

Lemmas

top wf, fpf-join wf, fpf-dom-list wf, isrcv wf, assert wf, fpf-dom wf, assert-has-src, da-outlink-f wf, has-src wf, member map filter, fpf-trivial-subtype-top, Id wf, IdLnk wf, Knd wf, fpf wf, Kind-deq wf, da-outlinks wf, l member wf, decidable assert, sq stable from decidable, assert-deq-member, subtype rel list, select wf, length wf1, tagof wf, lnk wf, not wf, bnot wf, fpf-ap wf, bool wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, fpf-join-ap-sq, fpf-join-dom